
module TravelDream


sig Persona{
amici: Persona,
prenotazioni: Pacchetto,
email: one Email
}

sig Email{}



abstract sig Componente{
data: Int,
city: one City
}{
data >0		//non necessario, ma rende più facile controllare che i vincoli siano rispettitati
}

//Voli
sig Voli extends Componente{
cityArrivo: one City
}

//Escursioni
sig Escursioni extends Componente{}

//Alberghi
sig Alberghi extends Componente{
dataFine: Int
}


//Citta
sig City{
regione: one Regione
}

sig Regione{
nazione: one Nazione
}

sig Nazione{}



//Pacchetti
sig Pacchetto{
voli: set Voli,
alberghi: set Alberghi,
escursioni: set Escursioni,
pacchettoPredef: set PacchettoPredef
}


//Pacchetti predefiniti
sig PacchettoPredef{
voli: some Voli,
alberghi: some Alberghi,
escursioni: some Escursioni
}





//Devi lasciare l'albergo DOPO essere arrivato 
//(diversamente dagli aerei un albergo viene selezionato da una lista e
// quindi deve essere fatta questa assunzione)
fact{
no a:Alberghi | a.data  > a.dataFine
}

//Non devo avere alberghi voli o escursioni ripetute nel pacchetto se sono
//già nel pacchetto predefinito
fact{
no p:Pacchetto | p.voli  = p.pacchettoPredef.voli
no p:Pacchetto | p.alberghi  = p.pacchettoPredef.alberghi
no p:Pacchetto | p.escursioni  = p.pacchettoPredef.escursioni
}



//Non memorizzo nel database Nazioni e regioni se non associate a città
fact{
all n : Nazione | some r:Regione | n in r.nazione
all r : Regione | some c:City | r in c.regione
}

//i pacchetti predefiniti essendo creati da impiegati soddisfano i vincoli di consistenza
// come il fatto che gli alberghi e le escursioni sono inclusi tra due date di aerei diversi
fact{
all p: PacchettoPredef | 
	{all a:p.alberghi| some v:p.voli| a.data >= v.data
	  all a:p.alberghi| some v:p.voli| a.dataFine <= v.data
	}
}

fact{
all p: PacchettoPredef |
	{all e:p.escursioni| some v:p.voli|e.data >= v.data
	  all e:p.escursioni| some v:p.voli|e.data <= v.data
	}
}

//Una persona non può essere amica di se stessa
fact{
no p:Persona | p in p.amici
}

//Se una persona è amica con un'altra significa che hanno almeno un pacchetto in comune
fact{
all p1:Persona{
	all p2:p1.amici| some pre:p1.prenotazioni| pre in p2.prenotazioni
	}
}
//Non vengono considerate le persone che non hanno accettato inviti


//Un pacchetto può appartenere solo a un gruppo di amici, non a persone estranee
/*fact{
all p1:Persona{
	all pre:p1.prenotazioni| some p2:Persona | (p2 not in p1.amici) && (pre in p2.prenotazioni)
	}
}*/

fact{
all p1:Persona{
	all p2:Persona |
		{  all pre:p1.prenotazioni|
			 (((p1!=p2) && (p2 not in p1.^amici))  => (pre not in p2.prenotazioni))
		}
	}
}

//Una email può essere di un' unica persona
fact{
all  p1:Persona | all p2:Persona| (p1!=p2) => (p1.email!=p2.email)
}


pred aggiungiVolo[p,p':Pacchetto, v:Voli]{
 v not in p.voli => p'.voli= p.voli+v
}


pred show {
#Persona=2
#Pacchetto =2
#City = 1
}
run show for 5

